A:Type, f:a:A fp Type, eq:EqDecider(A), x:A, z:Type. f(x)?z  Type 

latex

Definitions	x:A. B(x), t  T, f(x)?z, if b then t else f fi , x. t(x), P  Q, tt, ff, , , x(s), Unit, P  Q, P & Q,
Lemmas	fpf-dom wf, fpf-trivial-subtype-top, bool wf, eqtt to assert, fpf-ap wf, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, deq wf, fpf wf